\documentclass[a4paper]{article}
\usepackage{url}
\author{Dag Hovland}
\title{Report on the prover \emph{clp}}
\begin{document}
\maketitle
\begin{abstract}
  \emph{clp} (Coherent Logic Prover) is a prover for coherent logic developed by the author. It takes as input first order logic theories in coherent form. The present report first explains the usage of clp, then turns to a more detailed description of its internals.
\end{abstract}
\section{Overview and Features}
Motivation and theoretical background can be found in \emph{Efficient Rule-Matching for Hyper-Tableaux
}, available at \url{heim.ifi.uio.no/martingi/pub/iwil12.pdf}.
\subsection{Running clp}
clp is run from the command-line. An overview of the command-line options is seen when giving the option \verb|--help|. The name of the file with the coherent theory comes after the options. 

\subsection{Input}
clp recognizes two different syntaxes for the input, which are chosen by the argument \verb|--CL.pl| or \verb|--geolog|. \verb|--CL.pl| is used for the prolog-like format also used by the prover CL.pl by Marc Bezem. This is the default input format. The strategy information supported by CL.pl is though not supported by clp, and is ignored. \verb|--geolog| enables the format used by the prover Geolog, by John Fisher.


Equality is not supported by the prover and must be axiomatized or treated otherwise in the theory. Function symbols in terms are supported. The CL.pl and geolog format assumes theories with no rigid variables. To remove rigid variables from theories it is usual to introduce a domain predicate. The prover assumes that \verb|dom| is the name of this predicate. (This can be changed in the file common.h). %The prover will still work when using other names for the domain predicate, but it might be slower. 

\subsection{Output}
The prover can be configured to output information about every rule instance application, or to give no output at all during the proof search. (See information about running clp below.) If the prover in some branch cannot apply any rule instance, it will halt, and output the present fact-set / model. The latter output may be suppressed by command-line options. 

If all branches end with a contradiction, a proof of contradiction in coq format may be output. The proof in coq is based on use of the tactics \verb|apply|, \verb|elim|, \verb|intro|, \verb|split| and \verb|assumption|. The proof processes in coherent provers and using tactics in coq go in opposite directions: Coq starts with the goal, and then tactics can be used to apply axioms backwards to find the necessary premises, while coherent logic provers start with the premises and try to infer the goal. This makes it necessary to do some restructuring of the proof to enable coq output. The code for this is found in the files \verb|prover|\underline{ }\verb|single.c| and \verb|proof|\underline{ }\verb|writer.c|. Proof output is disabled by default.

\subsection{The Proof Search}
The prover uses the Rete algorithm for the matching during the proof search. This is explained in the paper, but some comments are in order. The matching inside Rete is somewhat parallelized: The nodes that are connected to a single axiom (not shared between several axioms) are treated by separate threads. There is one thread running for each axiom, and this thread reads from a queue of inserted matches, and outputs a list of applicable instances. These threads are also \emph{lazy} in the sense that they only read from the input queue if there are no instances on the output queue. This laziness may prevent the construction of large queues of applicable rule instances. The output queues from these threads are read by the prover to find what new applicable instance are available. The choice of which instance to apply is determined by the strategy, defined in \verb|strategy.c|.

\subsection{Timestamps and Substitutions}
Each application of a rule instance is called a \emph{step} and is given a unique \emph{timestamp}, starting with $1$ and increasing. This timestamp is also the index to an array where all rule instance applications are stored. 
A rule instance in the prover contains a link to an axiom and to a substitution. The substitution contains a mapping from variables to terms. In addition, each substitution contains a list of the timestamps of all rule instance applications that were causing the rule instance to be applicable. When the rete network constructs unions of substitutions, also the union of the timestamp lists are taken.

\subsubsection{Pruning}
Each applied rule instance is stored in an array during the proof. Together with the axiom and substitution is also information about which previous steps enabled this rule to be applied. This information is necessary for the construction of the coq proof, which goes in the opposite direction of the coherent proof, and for what is commonly called pruning. Whenever a contradiction is reached, the links to previous rule instances are followed recursively, and each instance that is met, is marked as used. Whenever a branch finishes, the prover checks whether the disjunction itself is marked as used. If it is not, then the contradiction can be proved without use of the instance of the disjunction, and the remaining branches need not be treated. The other branches are \emph{pruned}.

\subsection{Backtracking}
When a branch is finished, the prover \emph{backtracks} up to the previous disjunction. Almost all data structures allocated when treating the branch are deallocated. Since all the data that can be deallocated is stored in large arrays, the deallocation reduces to decrementing the indices to the next free elements in these arrays. This index value is stored by the prover when starting to treat a disjunction.

\section{Usage}
This section contains practical information about obtaining and running clp.
\subsection{Obtaining clp}
The source code of clp, and example theories, can be download from \url{http://code.google.com/p/clp}. It has only been tested on GNU/linux. For compilation it requires recent versions of bison and flex. It is compiled with the usual configure and make scripts, as described in the files \verb|README| and \verb|INSTALL|. \verb|make all| compiles the main executable clp, while \verb|make check| also compiles clpdebug and clpmemdebug which are used for debugging purposes


\subsection{Limiting the Prover}
There are three command-line options for limiting how long the prover runs. If none of these limits are set, the prover runs until it either finds a proof of contradiction, if finds a model of the theory, it runs out of memory or is aborted by other means. \verb|--wallclocktimer| limits the number of seconds that may pass from the prover is started until it is halted. \verb|--cputimer| limits the number of second of cpu time the prover may use. \verb|--max| limits the number of inference steps that may be taken, $0$ means unlimited. The latter is by default set to $300$.

\subsection{Output}
If the \verb|--verbose| option is given, the prover outputs information about each step taken. More information may be given by combinations of the \verb|--debug| option and uncommenting definitions in \verb|src/common.h|. 
If the \verb|--coq| option is given and a proof is found, the proof is translated to the coq format and output as a \verb|.v| file. \verb|--print|\underline{ }\verb|model| prints the model if one is found


The remaining options are mainly for experimenting with different variations of the prover internals. 

\section{Internals of the Prover}

\subsection{Parsing}
Parsing and lexing is done by bison and flex, respectively, and the source code is in the files with suffix .l and .y for the different formats: geolog and clpl. 

The parser returns a \verb|theory| (defined in theory.h) which contains all the axioms, and also auxiliary information like the names of all variables, constants, function names, and predicates occurring in the theory. 

\subsection{Construction of the Rete network}
The \verb|theory| struct is passed to the function \verb|create|\underline{ }\verb|rete|\underline{ }\verb|net| (together with info about commandline options.) This construction is sketched in other papers, but some points will be noted: The net is accessed by through the struct \verb|rete|\underline{ }\verb|net| defined in rete\underline{ }net.h. The latter structure contains a pointer to each selector (top-level $\alpha$-node) and to each rule-node. In addition information about many command-line switches is stored in this structure. 

\subsection{The Proof Search}
The function \verb|prover|\underline{ }\verb|single| in prover.c represents the proof search itself, and is passed a \verb|rete|\underline{ }\verb|net| as its single argument. The latter is never changed inside this function. Instead, a different struct \verb|rete_state_single| is used to store all the \verb|rete|\underline{ }\verb|net|. After some initial setup (initializing the fact-set etc.) the function passes control to  \verb|run|\underline{ }\verb|prover|\underline{ }\verb|single| which contains the main loop of the program;: a while-loop which iterates once for each \emph{step} taken by the prover. Each such step starts with determining the next rule instance to apply. This is done by a call to the function \verb|choose_next_instance_single|, which is mainly a wrapper to a call to the function in strategy.c coresponding to the chosen strategy. See more about strategy.c below.

\subsection{Datatypes for logical expressions}
A term is a constant, a variable, or a function applied to a list of terms. Terms are defined in term.h and the functions are in atom\underline{ }and\underline{ }term.c. 

Atoms are defined in atom.h and the functions are in atom\underline{ }and\underline{ }term.c

Initially, the domain is assumed to be exactly the constants appearing in the theory. These are stored in the struct \verb|constants|. When the prover applies existential clauses, new elements may be added to this structure. 

\subsection{Strategies}
With a strategy for the prover, we mean how the next rule instance application is chosen. The code for this choice is in the function \verb|normal|\underline{ }\verb|next|\underline{ }\verb|instance| in strategy.c. The present strategy is based on some rather intuitive heuristics. \verb|clpl|\underline{ }\verb|next|\underline{ }\verb|instance| implements a depth-first strategy, trying to simulate the strategy used by the prover CL.pl. Adding more strategies should not be hard.



\end{document}